Nuprl Lemma : mon_assoc
13,42
postcript
pdf
g
:IMonoid,
a
,
b
,
c
:|
g
|. (
a
* (
b
*
c
)) = ((
a
*
b
) *
c
)
|
g
|
latex
Up
groups
1
Definitions of Statement
IsMonoid(
T
;
op
;
id
)
,
IMonoid
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
IMonoid
,
P
&
Q
,
IsMonoid(
T
;
op
;
id
)
,
Assoc(
T
;
op
)
Lemmas
imon
wf
,
imon
properties
origin
g:IMonoid, a, b, c:|g|. (a * (b * c)) = ((a * b) * c) 
|g| g:IMonoid, a, b, c:|g|. (a * (b * c)) = ((a * b) * c) |g| Tx:A. B(x)